The main visible change in Elpi 2.0 is that the compiler performs type checking incrementally (as units gets added to the base program) and reports error messages with a precise location. The new type checker is written in OCaml and is much faster, but a bit less permissive. Before this PR all type declarations were merged together before type checking the entire program. With Elpi 2.0 compilation units need to type check using the types declared inside them (or in the base they extend).

Elpi Typecheck becomes useless.

A subtle difference is that rules belonging to a Db are type checked against the Db only, not the programs that uses them or the program that generates them.
This means Db rules "work" in the context of any Db user. But rules cannot call any of the code of these programs (the type checker complains about undefined symbols). Unless the types of the predicates they call are also declared in the Db (not necessarily their code: ensuring that the code is finally available is left to the programmer for now). Elpi Accumulate dbname File name. can mitigate this issue by putting in name the code (or at least the type declarations) needed by the rules in the Db.

This PR also adds Elpi File name code. to declare a (virtual) file that can be easily accumulated to Dbs or Programs.

This PR also adds a scope attribute to Elpi Accumulate, in particular #[superglobal] Elpi Accumulate dbname File stuff ensure the Db always contains stuff (a bit like it did always contain its header).

This PR adds a new command Elpi Accumulate Db Header to accumulate the header (type declaration typically) of a Db but not its code. The idiom is to accumulate the Db header early and the Db contents late. This can speed up the (re)compilation of large programs when the db is extended.

TODO:

• Elpi Accumulate File Signature foo.